Yet another proof of Goedel's completeness theorem for first-order classical logic

摘要

A Henkin-style proof of completeness of first-order classical logic is givenwith respect to a very small set (notably missing cut rule) of Genztendeduction rules for intuitionistic sequents. Insisting on sparing on derivationrules, satisfiability theorem is seen to need weaker assumptions thancompleteness theorem, the missing request being exactly the rule ~ p --> p,which gives a hint of intuitionism's motivations from a classical point ofview. A bare treatment of standard, basic first-order syntax somehow morealgebraic-flavoured than usual is also given.